(set-logic QF_IDL)
(declare-fun v0 () Int)
(assert (let ((e1 409333586))
(let ((e2 4726110))
(let ((e3 61))
(let ((e4 15015816))
(let ((e5 (< v0 v0)))
(let ((e6 (distinct v0 v0)))
(let ((e7 (>= (- v0 v0) (- e4))))
(let ((e8 (= v0 v0)))
(let ((e9 (distinct (- v0 v0) (- e3))))
(let ((e10 (>= (- v0 v0) e1)))
(let ((e11 (<= (- v0 v0) (- e3))))
(let ((e12 (>= (- v0 v0) (- e3))))
(let ((e13 (< (- v0 v0) e4)))
(let ((e14 (< v0 v0)))
(let ((e15 (distinct v0 v0)))
(let ((e16 (distinct (- v0 v0) e1)))
(let ((e17 (>= (- v0 v0) e4)))
(let ((e18 (distinct v0 v0)))
(let ((e19 (> v0 v0)))
(let ((e20 (= v0 v0)))
(let ((e21 (>= v0 v0)))
(let ((e22 (<= v0 v0)))
(let ((e23 (> (- v0 v0) e1)))
(let ((e24 (> v0 v0)))
(let ((e25 (> v0 v0)))
(let ((e26 (> (- v0 v0) e4)))
(let ((e27 (<= (- v0 v0) e2)))
(let ((e28 (= (- v0 v0) (- e3))))
(let ((e29 (<= v0 v0)))
(let ((e30 (<= v0 v0)))
(let ((e31 (< (- v0 v0) e1)))
(let ((e32 (<= (- v0 v0) e3)))
(let ((e33 (<= (- v0 v0) e4)))
(let ((e34 (< v0 v0)))
(let ((e35 (> (- v0 v0) e3)))
(let ((e36 (>= (- v0 v0) (- e3))))
(let ((e37 (< v0 v0)))
(let ((e38 (> v0 v0)))
(let ((e39 (= v0 v0)))
(let ((e40 (distinct (- v0 v0) (- e3))))
(let ((e41 (< (- v0 v0) (- e4))))
(let ((e42 (distinct v0 v0)))
(let ((e43 (= v0 v0)))
(let ((e44 (distinct v0 v0)))
(let ((e45 (= v0 v0)))
(let ((e46 (= v0 v0)))
(let ((e47 (<= (- v0 v0) (- e1))))
(let ((e48 (<= v0 v0)))
(let ((e49 (>= v0 v0)))
(let ((e50 (= (- v0 v0) (- e4))))
(let ((e51 (>= (- v0 v0) (- e1))))
(let ((e52 (<= (- v0 v0) (- e1))))
(let ((e53 (> v0 v0)))
(let ((e54 (xor e33 e50)))
(let ((e55 (ite e30 e14 e24)))
(let ((e56 (=> e45 e16)))
(let ((e57 (xor e15 e53)))
(let ((e58 (not e26)))
(let ((e59 (=> e43 e21)))
(let ((e60 (ite e22 e19 e5)))
(let ((e61 (= e47 e57)))
(let ((e62 (or e20 e42)))
(let ((e63 (ite e34 e38 e13)))
(let ((e64 (ite e23 e41 e46)))
(let ((e65 (=> e36 e17)))
(let ((e66 (not e61)))
(let ((e67 (=> e60 e6)))
(let ((e68 (ite e56 e29 e63)))
(let ((e69 (= e28 e62)))
(let ((e70 (and e40 e67)))
(let ((e71 (xor e64 e52)))
(let ((e72 (ite e10 e55 e71)))
(let ((e73 (and e44 e58)))
(let ((e74 (or e69 e70)))
(let ((e75 (xor e73 e35)))
(let ((e76 (not e48)))
(let ((e77 (or e9 e72)))
(let ((e78 (not e12)))
(let ((e79 (xor e66 e25)))
(let ((e80 (xor e27 e32)))
(let ((e81 (ite e49 e51 e7)))
(let ((e82 (= e37 e37)))
(let ((e83 (ite e80 e59 e54)))
(let ((e84 (ite e74 e31 e78)))
(let ((e85 (ite e75 e65 e84)))
(let ((e86 (and e8 e11)))
(let ((e87 (and e77 e77)))
(let ((e88 (not e85)))
(let ((e89 (xor e68 e39)))
(let ((e90 (or e79 e88)))
(let ((e91 (=> e81 e76)))
(let ((e92 (= e89 e18)))
(let ((e93 (=> e83 e83)))
(let ((e94 (= e93 e92)))
(let ((e95 (xor e86 e90)))
(let ((e96 (not e95)))
(let ((e97 (=> e82 e87)))
(let ((e98 (= e97 e94)))
(let ((e99 (and e91 e98)))
(let ((e100 (not e96)))
(let ((e101 (=> e100 e100)))
(let ((e102 (not e99)))
(let ((e103 (= e102 e102)))
(let ((e104 (= e103 e101)))
e104
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat-assuming ())
